$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $f$:($T$$\rightarrow$$T$), $x$:$T$. retraction($T$;$f$) $\Rightarrow$ ($f$$\ast\ast$($f$($x$)) = $f$$\ast\ast$($x$) $\in$ $T$)